nLab computable analysis

Idea

computability in analysis, constructive analysis

Related concepts

computability

	type I computability	type II computability
typical domain	natural numbers $\mathbb{N}$	Baire space of infinite sequences $\mathbb{B} = \mathbb{N}^{\mathbb{N}}$
computable functions	partial recursive function	computable function (analysis)
type of computable mathematics	recursive mathematics	computable analysis, Type Two Theory of Effectivity
type of realizability	number realizability	function realizability
partial combinatory algebra	Kleene's first partial combinatory algebra	Kleene's second partial combinatory algebra

• computable real number

• exact real computer arithmetic

• computable physics

References

A standard textbook is

• Klaus Weihrauch, Computable Analysis, Springer Berlin (2000)

A survey is in

• Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk, Constructive analysis, types and exact real numbers, Science Mathematical Structures in Computer Science / Volume 17 / Issue 01 / February 2007, pp 3-36 (publisher)

The Relation to realizability topos theory is discussed in

• P. Lietz, From constructive mathematics to computable analysis via the realizability interpretation , Ph.D. dissertation, Fachbereich Mathematik, TU Darmstadt, Darmstadt, 2004.

• Andrej Bauer, The realizability approach to computable analysis and topology, Ph.D. dissertation, School of Computer Science, Carnegie Mellon University, Pittsburgh, 2000.

• Andrej Bauer, Realizability as connection between constructive and computable mathematics, in T. Grubba, P. Hertling, H. Tsuiki, and Klaus Weihrauch, (eds.) CCA 2005 - Second International Conference on Computability and Complexity in Analysis, August 25-29,2005, Kyoto, Japan, ser. Informatik Berichte, , vol. 326-7/2005. FernUniversität Hagen, Germany, 2005, pp. 378–379. (pdf)